(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #xe63bb02db51cecba) #xce227e9257189a2f))
(constraint (= (f #xc410dbcae56da486) #xdf7921a8d492dbcf))
(constraint (= (f #x3185565b57976cad) #x73d54d2543449a97))
(constraint (= (f #x2e4601e6725316d7) #x68dcff0cc6d67494))
(constraint (= (f #xcd92283e0ce3477a) #x1936ebe0f98e5c42))
(constraint (= (f #x5dc378b2a44a205b) #x511e43a6addaefd2))
(constraint (= (f #x48c840d07a4d4623) #xb9bdf97c2d95cee7))
(constraint (= (f #xea58ed5008a06048) #x0ad38957fbafcfdb))
(constraint (= (f #x1ade42058428288a) #x7290defd3debebba))
(constraint (= (f #xce5bd32d62e0d370) #x18d216694e8f9647))
(constraint (= (f #x4c73aae1ae705ad2) #x59c62a8f28c7d296))
(constraint (= (f #x96398403c4b4441b) #x4e33dfe1da5ddf27))
(constraint (= (f #x6eed684d001cdc4d) #x8894bd97ff191d97))
(constraint (= (f #x4ac3bbebeb7337ed) #x5a9e220a0a466409))
(constraint (= (f #x737dcb7e836e3662) #x6411a40be48e4cef))
(constraint (= (f #xdb6450414edc0ae9) #x24dd7df5891fa8b7))
(constraint (= (f #x6e8c1715cd730e1e) #x48b9f475194678f0))
(constraint (= (f #xeadb0b3188143a2b) #xa927a673bf5e2ea7))
(constraint (= (f #x65ceddea6d16eb3d) #xd18910ac9748a617))
(constraint (= (f #xa36c60e54eb91e7d) #x2e49cf8d58a370c1))
(constraint (= (f #x9cb4a3cdca7b58e0) #x31a5ae191ac2538f))
(constraint (= (f #x46093bec1148cecb) #x5cfb6209f75b989a))
(constraint (= (f #xb5c449ce6b34a962) #x51ddb18ca65ab4ef))
(constraint (= (f #x57bdd63e38ee1c81) #x42114e0e388f1bf7))
(constraint (= (f #xd8777c492a59ddde) #x13c441db6ad31110))
(constraint (= (f #xe44a6ec5e5b7bd15) #xddac89d0d2421757))
(constraint (= (f #x6bbcb3eed2a70a10) #xa21a60896ac7af7f))
(constraint (= (f #x7d7e37e9916b7253) #x4140e40b374a46d6))
(constraint (= (f #xa96e325cb2bd08ee) #xb48e6d1a6a17b88f))
(constraint (= (f #xb6e1db10c3b00006) #x248f12779e27fffc))
(constraint (= (f #x2daa96d3368b38e2) #x692ab49664ba638e))
(constraint (= (f #x00bce3e5b1b9634a) #x7fa18e0d27234e5a))
(constraint (= (f #x14864aae2981344d) #x75bcdaa8eb3f65d9))
(constraint (= (f #x52e454e254697d2e) #x568dd58ed5cb4168))
(constraint (= (f #x7ed4ecb8e9c0c4b4) #x409589a38b1f9da5))
(constraint (= (f #xdb253472d135422e) #x26d65c697655ee8f))
(constraint (= (f #x84cba1d019532c1e) #x3d9a2f17f35669f0))
(constraint (= (f #xea7e561096a091a1) #x0ac0d4f7b4afb72f))
(constraint (= (f #x4b7d96371220c126) #x5a4134e476ef9f6c))
(constraint (= (f #x7482741889d054e3) #x45bec5f3bb17d58e))
(constraint (= (f #x3129203b20942a3d) #x76b6fe26fb5eae17))
(constraint (= (f #x905492765e814b7c) #x37d5b6c4d0bf5a41))
(constraint (= (f #x537e142eee84e934) #x640f5e888bd8b65f))
(constraint (= (f #x2a5e427d504d7371) #xad0dec157d946477))
(constraint (= (f #xa6aea8ea03116e4d) #x2ca8ab8afe7748d9))
(constraint (= (f #xe6e93e74eec64c1c) #xc8b60c5889cd9f1f))
(constraint (= (f #xe492e2db0c05d518) #xdb68e9279fd1573f))
(constraint (= (f #x180e9c81d959501b) #x73f8b1bf135357f2))
(constraint (= (f #x5798736e89be4786) #x433c648bb20dc3cf))
(constraint (= (f #xa3c5124c822ccebb) #xe1d76d9bee998a27))
(constraint (= (f #x44439e553553928a) #x5dde30d5655636ba))
(constraint (= (f #x691cd532b6e1e8c2) #x4b719566a48f0b9e))
(constraint (= (f #x0d612eb9e73d5701) #x94f68a30c61547f7))
(constraint (= (f #xe57dc8636c553042) #xd411bce49d567def))
(constraint (= (f #x39178e7e49490643) #x637438c0db5b7cde))
(constraint (= (f #xe34ad23cca051456) #xe5a96e19afd75d4f))
(constraint (= (f #xa925854e0c859471) #xb6d3d58f9bd35c77))
(constraint (= (f #xe7de438524bb337c) #x0c10de3d6da26641))
(constraint (= (f #x84943e780c7ad7ee) #x3db5e0c3f9c29408))
(constraint (= (f #xcc05e6be59adda1d) #x9fd0ca0d32912f17))
(constraint (= (f #x379b27acbcdc5751) #x4326c29a191d4577))
(constraint (= (f #x70ab3ab21a795e59) #x47aa62a6f2c350d3))
(constraint (= (f #xe8422981d005c082) #xbdeeb3f17fd1fbef))
(constraint (= (f #xa5e6d309937d0cee) #xd0c967b36417988f))
(constraint (= (f #xc925c05cb3aeba58) #xb6d1fd1a628a2d3f))
(constraint (= (f #x4a52b12c8bc05ee9) #x5ad6a769ba1fd08b))
(constraint (= (f #x87e3e02a010784b3) #xc0e0feaff7c3da67))
(constraint (= (f #xab5e0078d03be0b7) #x2a50ffc397e20fa4))
(constraint (= (f #x68762e28776e97ca) #xbc4e8ebc448b41af))
(constraint (= (f #xc2415419928b9e5e) #x1edf55f336ba30d0))
(constraint (= (f #x9ee45eaa01c0a415) #x308dd0aaff1fadf5))
(constraint (= (f #x433390466e81dbe0) #x5e6637dcc8bf120f))
(constraint (= (f #x202dc2d2eb341ed1) #xfe91e968a65f0977))
(constraint (= (f #xbe693d078de596c0) #x0cb617c390d349ff))
(constraint (= (f #x0c8d1837982e6719) #x9b973e433e8cc737))
(constraint (= (f #x49e5be71c7675497) #xb0d20c71c4c55b47))
(constraint (= (f #x82a74944d129162c) #x3eac5b5d976b74e9))
(constraint (= (f #xacee7e8113bbea78) #x2988c0bf76220ac3))
(constraint (= (f #xc961cb03ddcce2e6) #xb4f1a7e11198e8cf))
(constraint (= (f #x7c08a7dc38438985) #x41fbac11e3de3b3d))
(constraint (= (f #x7e23e27620da0e0c) #x40ee0ec4ef92f8f9))
(constraint (= (f #x389ee20deecce7dd) #x3b08ef908998c117))
(constraint (= (f #x8ecb0233a95026d2) #x389a7ee62b57ec96))
(constraint (= (f #xad5973d42009146e) #x29534615effb75c8))
(constraint (= (f #x1c342375637d7469) #x1e5ee454e4145cb7))
(constraint (= (f #x1d2e953ce71ccdb9) #x168b5618c7199237))
(constraint (= (f #x1523ca82e45e78c2) #x56e1abe8dd0c39ef))
(constraint (= (f #x92263bbc91c95a28) #x36ece221b71b52eb))
(constraint (= (f #x1543e3db9ac5354d) #x55e0e12329d65597))
(constraint (= (f #x89207c9e4709cc9a) #x3b6fc1b0dc7b19b2))
(constraint (= (f #x2830119395e1b2ce) #x6be7f736350f2698))
(constraint (= (f #xc0b441da18e4ece2) #xfa5df12f38d898ef))
(constraint (= (f #x9ac70dd6e8d3ebed) #x329c79148b960a09))
(constraint (= (f #xab152ace7517ad64) #xa756a98c574294df))
(constraint (= (f #xbd04d5a54391569e) #x217d952d5e3754b0))
(constraint (= (f #x60caa502c0edb4c0) #xf9aad7e9f89259ff))
(constraint (= (f #xd0852e2b54b39ee8) #x17bd68ea55a6308b))
(constraint (= (f #xb81d5a3c319dd5e5) #x3f152e1e731150d7))
(constraint (= (f #x7199e72a89613e5a) #x47330c6abb4f60d2))
(constraint (= (f #xdda577d43ce6c119) #x12d4415e18c9f737))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvashr x x) #x0000000000000000) (ite (= (bvurem x #x000000000000000d) #x0000000000000002) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvor #x0000000000000002 x) x) (ite (= (bvurem x #x0000000000000006) #x0000000000000001) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvor #x000000000000000c x) x) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x000000000000000a) #x0000000000000000) (bvnot (bvmul #x0000000000000008 x)) (ite (= (bvor #x0000000000000008 x) x) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x000000000000000e) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvsrem x #x000000000000000d) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x0000000000000006) #x0000000000000002) (ite (= (bvor #x0000000000000004 x) x) (bvudiv (bvnot x) #x0000000000000002) (bvnot (bvmul #x0000000000000008 x))) (bvnot (bvmul #x0000000000000008 x)))))))))) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (ite (= (bvurem x #x000000000000000d) #x0000000000000001) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvor #x0000000000000008 x) x) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvnot (bvmul #x0000000000000008 x)) (ite (= (bvurem x #x0000000000000003) #x0000000000000002) (ite (= (bvsrem x #x0000000000000005) #x0000000000000001) (bvudiv (bvnot x) #x0000000000000002) (bvnot (bvmul #x0000000000000008 x))) (bvudiv (bvnot x) #x0000000000000002))) (bvnot (bvmul #x0000000000000008 x)))) (bvnot (bvmul #x0000000000000008 x))))) (ite (= (bvurem x #x000000000000000a) #x0000000000000001) (bvnot (bvmul #x0000000000000008 x)) (ite (= (bvand #x000000000000000b x) #x0000000000000002) (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x000000000000000b) #x0000000000000002) (bvudiv (bvnot x) #x0000000000000002) (bvnot (bvmul #x0000000000000008 x)))) (ite (= (bvurem x #x0000000000000007) #x0000000000000002) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x0000000000000007) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x000000000000000f) #x0000000000000001) (bvnot (bvmul #x0000000000000008 x)) (ite (= (bvurem x #x0000000000000009) #x0000000000000002) (bvnot (bvmul #x0000000000000008 x)) (ite (= (bvor #x0000000000000007 x) x) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvsrem x #x0000000000000005) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvand #x000000000000000b x) #x0000000000000000) (bvnot (bvmul #x0000000000000008 x)) (ite (= (bvurem x #x000000000000000a) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvurem x #x000000000000000b) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvsrem x #x0000000000000006) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvsrem x #x0000000000000009) #x0000000000000000) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvor #x0000000000000002 x) x) (bvnot (bvmul #x0000000000000008 x)) (ite (= (bvurem x #x000000000000000b) #x0000000000000002) (bvudiv (bvnot x) #x0000000000000002) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (ite (= (bvurem x #x0000000000000005) #x0000000000000000) (bvnot (bvmul #x0000000000000008 x)) (bvudiv (bvnot x) #x0000000000000002)) (bvnot (bvmul #x0000000000000008 x))))))))))))))))))))
